(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_20 (Sun Microsystems Inc.) Main-Class: CyclicPair2
public class CyclicPair2 {
CyclicPair2 next;

public static void main(String[] args) {
Random.args = args;
CyclicPair2 one = new CyclicPair2();
CyclicPair2 two = new CyclicPair2();
int rand = Random.random();
if (rand != 0) {
one.next = two;
two.next = one;
} else {
one.next = two;
}

if (rand == 0) {
one.run();
}
}

public void run() {
CyclicPair2 current = this;
while (current != null)
current = current.next;
}
}


public class Random {
static String[] args;
static int index = 0;

public static int random() {
String string = args[index];
index++;
return string.length();
}
}


(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
CyclicPair2.main([Ljava/lang/String;)V: Graph of 131 nodes with 0 SCCs.


(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Logs:

(4) TRUE